home *** CD-ROM | disk | FTP | other *** search
/ Tech Arsenal 1 / Tech Arsenal (Arsenal Computer).ISO / tek-04 / prolog_2.zip / CAD.ZIP / ATGS.PRO < prev    next >
Text File  |  1987-04-05  |  15KB  |  515 lines
  1. /*
  2. .pn1
  3. .he                           DREXEL ATGS */ 
  4.  
  5. constrainlist( [constraint1] ).
  6.  
  7. constraint1( pc_inv, pdcfinv, pcinv ).
  8. buf(  pc_buf,  pdcfbuf,  pcbuf ).
  9. and2( pc_and2, pdcfand2, pcand2 ).
  10. and3( pc_and3, pdcfand3, pcand3 ).
  11. or2( pc_or2, pdcfor2, pcor2 ).
  12. or3( pc_or3, pdcfor3, pcor3 ).
  13.  
  14. /* The primitive cubes of the logic elements.
  15. Form: pc_type( output, [list of prime implicants] ). */
  16.  
  17. pc_inv( 0, [[1]] ).
  18. pc_inv( 1, [[0]] ).
  19. pc_buf( 0, [[0]] ).
  20. pc_buf( 1, [[1]] ).
  21. pc_and2( 0, [[0,_],[_,0]] ).
  22. pc_and2( 1, [[1,1]] ).
  23. pc_and3( 0, [[0,_,_],[_,0,_],[_,_,0]] ).
  24. pc_and3( 1, [[1,1,1]] ).
  25.  
  26. pc_or2( 1, [[1,_],[_,1]] ).
  27. pc_or2( 0, [[0,0]] ).
  28. pc_or3( 1, [[1,_,_],[_,1,_],[_,_,1]] ).
  29. pc_or3( 0, [[0,0,0]] ).
  30.  
  31.  
  32. /* The primitive D-cubes of the logic elements: */
  33.  
  34. pdcfinv(  sa0(_), db, [[1]] ).
  35. pdcfinv(  sa1(_), d,  [[0]] ).
  36. pdcfbuf(  sa0(_), d,  [[1]] ).
  37. pdcfbuf(  sa1(_), db, [[0]] ).
  38. pdcfand2( sa0(_), d,  [[1,1]] ).
  39. pdcfand2( sa1(1), db, [[0,1]] ).
  40. pdcfand2( sa1(2), db, [[1,0]] ).
  41. pdcfand3( sa0(_), d,  [[1,1,1]] ).
  42. pdcfand3( sa1(1), db, [[0,1,1]] ).
  43. pdcfand3( sa1(2), db, [[1,0,1]] ).
  44. pdcfand3( sa1(3), db, [[1,1,0]] ).
  45.  
  46. pdcfor2( sa0(1), d, [[1,0]] ).
  47. pdcfor2( sa0(2), d, [[0,1]] ).
  48. pdcfor2( sa1(_), db, [[0,0]] ).
  49.  
  50. pdcfor3( sa0(1), d, [[1,0,0]] ).
  51. pdcfor3( sa0(2), d, [[0,1,0]] ).
  52. pdcfor3( sa0(3), d, [[0,0,1]] ).
  53. pdcfor3( sa1(_), db, [[0,0,0]] ).
  54.  
  55. /* The propagation D-cubes of the logic elements: */
  56.  
  57. pcinv( d,  [[db]] ).èpcinv( db, [[d]] ).
  58. pcbuf( d, [[d]] ).
  59. pcbuf( db, [[db]] ).
  60. pcand2( d, [[1,d],[d,1],[d,d]] ). 
  61. pcand2( db,[[1,db],[db,1],[db,db]] ).
  62. pcor2( d, [[0,d],[d,0,],[d,d]] ).
  63. pcor2( db, [[0,db],[db,0],[db,db]] ).
  64. pcand3( d, 
  65.   [[d,1,1],[1,d,1],[1,1,d],[d,d,1],[d,1,d],[1,d,d],[d,d,d]] ).
  66. pcand3( db,
  67.   [[db,1,1],[1,db,1],[1,1,db],[db,db,1],[db,1,db],[1,db,db],[db,db,db]] ).
  68. pcor3( d,
  69.   [[d,0,0],[0,d,0],[0,0,d],[d,d,0],[d,0,d],[0,d,d],[d,d,d]] ).
  70. pcor3( db,
  71.   [[db,0,0],[0,db,0],[0,0,db],[db,db,0],[db,0,db],[0,db,db],[db,db,db]] ).
  72.  
  73.  
  74. /* Samples:
  75. Type:      and3( pdcfand3, pcand3 ).
  76. Pdcfclass: pdcfand3( sa1(3), db, [[1,1,0]] ).
  77. Gate:      r6( or3, 3, [n25,n26,n28], n34 ).
  78. */
  79.  
  80. /* Gatelines = [ [x,x,x], [x,x,x],..., [x,x,x] ] */
  81. /* Netnames =  [ nx(val), .... nx(val) ] */
  82.  
  83.  
  84.  
  85. /*
  86.    Netvals = current assignments of nets: [n1(1), n5(0),.....,nn(x)]
  87.    Inputnets = input nets to specific gate: [n1,n3,..nx]
  88.    Inputvals = [1,0,.d, db, 0]
  89. */
  90.  
  91.  
  92.  
  93.  
  94. listsubt( [], _, Res, Res ).
  95. listsubt( [Head|Mainlist], El, Buildlist, Result ) :-
  96.     (Head == El, listsubt( Mainlist, El, Buildlist, Result ));
  97.     listsubt( Mainlist, El, [Head|Buildlist], Result ), !.
  98.  
  99. findouttests( Gate, Fault ) :- 
  100.     print('\nSynthesizing Output Tests for: ', Gate, ' Fault: ', Fault ),
  101.     memleft( Memleft1 ),
  102.         print( '\nMemleft start gen: ', Memleft1 ),
  103.     (ftout( Gate, Fault ); true), 
  104.         !.
  105.  
  106. ftout( Gate, Fault ) :-
  107.     gentestoutp( Gate, Fault, TestInputs, TestOutputs ),
  108.     asserta( test( Gate, output, Fault, TestInputs, TestOutputs ) ),
  109.     print( '\n  Testinputs:  ', TestInputs ),
  110.     print( '\n  Testoutputs: ', TestOutputs ),
  111.     !,è        fail.
  112.  
  113.  
  114. findinptests( Gate, Input, Fault ) :- 
  115.     print('\nSynthesizing Input Tests for: ', Gate, ', Input: ', Input,
  116.              ' Fault: ', Fault ),
  117.     (ftinp( Gate, Input, Fault ); true), !.
  118.  
  119.  
  120. ftinp( Gate, Input, Fault ) :-
  121.     gentestinp( Gate, Input, Fault, TestInputs, TestOutputs ),
  122.     print( '\n  Testinputs:  ', TestInputs ),
  123.     print( '\n  Testoutputs: ', TestOutputs ), 
  124.     asserta( test( Gate, Input, Fault, TestInputs, TestOutputs ) ),
  125.         !,
  126.     fail.
  127.  
  128. /*
  129. ftinp( Gate, Input, Fault ) :-
  130.     !,
  131.     test( Gate, Input, Fault, TestInputs, TestOutputs ),
  132.     print( '\n  Testinputs:  ', TestInputs ),
  133.     print( '\n  Testoutputs: ', TestOutputs ),
  134.     fail.
  135. */
  136.  
  137.  
  138. gentestoutp( Gate, Fault, TestInputs, TestOutputs ) :-
  139.     Gate( Type, _, Inplist, Outnet ),
  140.     Type( Primcube, _, _ ),
  141.     elements( Ellist ),
  142.       listsubt( Ellist, Gate, [], Sublist ), !,
  143.     (
  144.           (
  145.             Fault == sa0, 
  146.         Primcube( 1, Implicants ),
  147.             member( Implicant, Implicants ),
  148.             pairoff( Inplist, Implicant, [], Netvals ),
  149.             ad_vals_to_Net( [Outnet(d)], Netvals, NNetvals )
  150.           );
  151.           (
  152.         Fault == sa1, 
  153.         Primcube( 0, Implicants ),
  154.             member( Implicant, Implicants ),
  155.             pairoff( Inplist, Implicant, [], Netvals ),
  156.             ad_vals_to_Net( [Outnet(db)], Netvals, NNetvals )
  157.       )
  158.         ),
  159.     outputs( Outlist ),
  160.     ( 
  161.           (
  162.             member( Outnet, Outlist ),
  163.             imply1( NNetvals, Sublist, NNNetvals, Undef ),
  164.             justify( NNNetvals, Undef, NNNNetvals ),
  165.             getinps( NNNNetvals, TestInputs ),è        getoutp( NNNNetvals, TestOutputs )
  166.           );
  167.           (
  168.             not( member( Outnet, Outlist ) ),
  169.             propagate( NNetvals, Sublist, 
  170.                                   NNNetvals, Undef, Solved ),
  171.             Solved == true,
  172.             justify( NNNetvals, Undef, NNNNetvals ),
  173.             getinps( NNNNetvals, TestInputs ),
  174.             getoutp( NNNNetvals, TestOutputs )
  175.           )
  176.         ).
  177.  
  178.  
  179.  
  180. gentestinp( Gate, Input, Fault, TestInputs, TestOutputs ) :-
  181.         Gate( Type, _, Inplist, Outnet ),
  182.         Type( _, Pdcfclass, _ ),
  183.         elements( Ellist ),
  184.         listsubt( Ellist, Gate, [], Sublist ),
  185.         !,
  186.     Pdcfclass( Fault(Input), Dtype, Implicants ),
  187.     member( Implicant, Implicants ),
  188.     pairoff( Inplist, Implicant, [], Netvals ),
  189.         outputs( Outlist ),
  190.         ( 
  191.           (
  192.             member( Outnet, Outlist ),
  193.             imply1( [Outnet(Dtype)|Netvals], Sublist, NNetvals, Undef ),
  194.             justify( NNetvals, Undef, NNNetvals ),
  195.             getinps( NNNetvals, TestInputs ),
  196.         getoutp( NNNetvals, TestOutputs )
  197.           );
  198.           (
  199.             not( member( Outnet, Outlist ) ),
  200.             propagate( [Outnet(Dtype)|Netvals], Sublist, 
  201.                                   NNetvals, Undef, Solved ),
  202.             Solved == true,
  203.             justify( NNetvals, Undef, NNNetvals ),
  204.             getinps( NNNetvals, TestInputs ),
  205.             getoutp( NNNetvals, TestOutputs )
  206.           )
  207.         ).
  208.  
  209. testfanouts :- testf; true.
  210.  
  211. testf :- 
  212.     findfanoutpts( Fans ), !,
  213.     print('\nElements with fanout:\n  ', Fans ),
  214.     member( Gate, Fans ),
  215.         memleft( Memleft1 ),
  216.         print( '\nMemleft start gen: ', Memleft1 ),
  217.     findouttests( Gate, sa0 ),
  218.         memleft( Memleft2 ),
  219.         print( '\nMemleft after sa0: ', Memleft2 ),è    findouttests( Gate, sa1 ),
  220.         memleft( Memleft3 ),
  221.         print( '\nMemleft after sa1: ', Memleft3 ),
  222.     fail.
  223.  
  224.  
  225. findfanoutpts( Netswfan ) :-
  226.     elements( Ellist ),
  227.     constrainlist( Constlist ),
  228.     ffo( Ellist, Constlist, [], Netswfan ), !.
  229.  
  230. ffo( [], _, Netform, Netform ).
  231. ffo( [El|Rem], Constlist, Netform, NetRet ) :-
  232.     (
  233.           El( Type, _, _, Outnet ),
  234.       not( member( Type, Constlist ) ),
  235.       Outnet( _, _, Inputlist ),
  236.           [H|T] = Inputlist, T \= [],
  237.       ffo( Rem, Constlist, [El|Netform], NetRet )
  238.         );
  239.     ffo( Rem, Constlist, Netform, NetRet ).
  240.  
  241. testoutputs :- testo ; true.
  242.  
  243. testo :- 
  244.     findoutputs( Outputs ), !,
  245.     member( Gate, Outputs ),
  246.         memleft( Memleft1 ),
  247.         print( '\nMemleft start gen: ', Memleft1 ),
  248.     findouttests( Gate, sa0 ),
  249.         memleft( Memleft2 ),
  250.         print( '\nMemleft after sa0: ', Memleft2 ),
  251.     findouttests( Gate, sa1 ),
  252.         memleft( Memleft3 ),
  253.         print( '\nMemleft after sa1: ', Memleft3 ),
  254.     fail.
  255.  
  256.  
  257.  
  258.  
  259. findoutputs( Netswfan ) :-
  260.     elements( Ellist ),
  261.     outputs( Outputs ),
  262.     fout( Ellist, Outputs, [], Netswfan ), !.
  263.  
  264. fout( [], _, Netform, Netform ).
  265. fout( [El|Rem], Outputs, Netform, NetRet ) :-
  266.     (
  267.           El( Type, _, _, Outnet ),
  268.           member( Outnet, Outputs ),
  269.       fout( Rem, Outputs, [El|Netform], NetRet )
  270.         );
  271.     fout( Rem, Outputs, Netform, NetRet ).
  272.  
  273. testinputs :- testi ; true.è
  274. testi :- 
  275.     findinputs( Inputs ), !,
  276.     member( [Gate,Input], Inputs ),
  277.         memleft( Memleft1 ),
  278.         print( '\nMemleft start gen: ', Memleft1 ),
  279.     findinptests( Gate, Input, sa0 ),
  280.         memleft( Memleft2 ),
  281.         print( '\nMemleft after sa0: ', Memleft2 ),
  282.     findinptests( Gate, Input, sa1 ),
  283.         memleft( Memleft3 ),
  284.         print( '\nMemleft after sa1: ', Memleft3 ),
  285.     fail.
  286.  
  287. findinputs( InpEls ) :-
  288.     elements( Ellist ),
  289.     inputs( Inputs ),
  290.     finp( Inputs, [], InpEls ), !.
  291.  
  292. finp( [], Netform, Netform ).
  293. finp(  [Inputnet|InpnetRem], Netform, NetRet ) :-
  294.     (
  295.           Inputnet( _, _, [El|_] ),
  296.           El( _, _, Nets, _ ),
  297.           member( Inputnet, Nets, Num ),
  298.           Numplus is Num + 1,
  299.       finp( InpnetRem, [[El,Numplus]|Netform], NetRet )
  300.         );
  301.     finp( ElRem, InpnetRem, Netform, NetRet ).
  302.  
  303.  
  304.  
  305. justify( Netvals, [], Netvals ).
  306. justify( Netvals, [El|Rem], NewNetReturn ) :-
  307.     El( Type, _, Inputs, Outnet ),
  308.         replcbyval( Netvals, Inputs, Vals, Varlist ),
  309.         Type( Pc, _, _ ),
  310.         (
  311.           (
  312.             member( Outnet(Output), Netvals ), 
  313.             !,
  314.             Pc( Output, Implicants ), 
  315.  
  316.             member( Implicant, Implicants ),
  317.  
  318.             Implicant = Vals,
  319.             ad_vals_to_Net( Netvals, Varlist, NNetvals ),
  320.         imply1( NNetvals, Rem, NNNewNet, Undef ),
  321.         justify( NNNewNet, Undef, NewNetReturn )
  322.           );
  323.       (
  324.             not( member( Outnet(Output), Netvals ) ),
  325.             justify( Netvals, Rem, NewNetReturn )
  326.           ) 
  327.         ).è
  328.  
  329.  
  330.  
  331.  
  332. propagate( Netvals, [], Netvals, [], _ ).
  333. propagate( Netvals, Ellist, NNNNetvals, UndefR, Solved ) :-
  334.     usecount(U),
  335.     imply1( Netvals, Ellist, NNetvals, UndefEllist ),
  336.     ddrive( NNetvals, UndefEllist, NNNetvals, [], 
  337.                               UndefEllist2, Solved, Drive  ),
  338.         (
  339.           (Solved == true, NNNNetvals = NNNetvals, UndefR = UndefEllist2, !); 
  340.           (
  341.             Drive == true,
  342.             propagate( NNNetvals, UndefEllist2, NNNNetvals, UndefR, Solved )
  343.           )
  344.         ).
  345.  
  346. /* Here [] is the empty list of elements currently in the D-frontier. */
  347.  
  348.  
  349.  
  350.  
  351. ddrive( Netvals, [], Netvals, Undef, UndefR, _, _  ) :-
  352.     revlist( Undef, UndefR ).
  353. ddrive( Netvals, [El|Remain], ReturnNewNet, Undefform, 
  354.                   Undefreturn, Solved, Drive ) :-
  355.     usecount(U),
  356.     El( Type, _, Inputs, Outnet ),
  357.     ( 
  358.           (
  359.         replcbyval( Netvals, Inputs, Vals, Varlist ),
  360.             hasD( Vals ),
  361.             Type( _, _, Prcube ),
  362.             Prcube( Output, Implicants ), 
  363.             member( Implicant, Implicants ), 
  364.             Implicant = Vals,
  365.             ad_vals_to_Net( Netvals, Varlist, NNetvals ),
  366.             notdup( Outnet, Output, Netvals, NNetvals, NNNetvals ),
  367.         Drive = true,
  368.             (
  369.               (
  370.                 outputs( Outlist ), 
  371.                 member( Outnet, Outlist ),
  372.             Solved = true, !,
  373.                 ReturnNewNet = NNNetvals,
  374.                 revlist( Undefform, UdfR ),
  375.                 appenddef( UdfR, Remain, Undefreturn )
  376.               );    
  377.               ddrive( NNNetvals, Remain, ReturnNewNet, 
  378.                           Undefform, Undefreturn, Solved, Drive  )
  379.             )
  380.           );(
  381.           ddrive( Netvals, Remain, ReturnNewNet, è                            [El|Undefform], Undefreturn, Solved, Drive  ))
  382.         ).
  383.  
  384.  
  385.  
  386. hasD( Inputs ) :- vmember( d, Inputs ); vmember( db, Inputs ).
  387.  
  388.  
  389. imply1( Netvals, Ellist, NNetvals, UndefEllist2 ) :-
  390.     imply( Netvals, Ellist, NNetvals, [], UndefEllist ),     
  391.     revlist( UndefEllist, UndefEllist2 ),
  392.     !.
  393.  
  394. imply( NewNetvals, [], NewNetvals, Undef, Undef ).
  395.  
  396. imply( Netvals, [El|Remain], ReturnNewNet, Undefform, Undefreturn ) :-
  397.         usecount(U),
  398.     El( Type, _, Inputs, Outnet ),
  399.         ( 
  400.           (
  401.           replcbyval( Netvals, Inputs, Vals, Varlist ),
  402.           not( hasD( Vals ) ),
  403.           Type( Pc, _, _ ),
  404.           Pc( Output, Implicants ), 
  405.           member( Implicant, Implicants ), 
  406.           Implicant == Vals,
  407.           notdup( Outnet, Output, Netvals, Netvals, NNNetvals ),
  408.           imply( NNNetvals, Remain, ReturnNewNet, Undefform, Undefreturn)
  409.           );
  410.           imply( Netvals, Remain, ReturnNewNet, [El|Undefform], Undefreturn) 
  411.         ).
  412.  
  413. notdup( Netval, Val, Netvals, NNetvals, NNetvals ) :-
  414.     member( Netval(Extval), Netvals ),
  415.     !,
  416.     Extval == Val.
  417.     
  418. notdup( Netval, Val, _, NNetvals, [Netval(Val)|NNetvals] ) :- !.
  419.  
  420.  
  421. ad_vals_to_Net( Netvals, Varlist, NewNet ) :-
  422.     advals( Netvals, Varlist, NewNet ), !.
  423. advals( Netvals, [], Netvals ).
  424. advals( Netvals, [Head(Val)|Varlist], NNetvalsR ) :-
  425.     (
  426.           (
  427.             atomic(Val),
  428.         advals( [Head(Val)|Netvals], Varlist, NNetvalsR )
  429.           );
  430.           advals( Netvals, Varlist, NNetvalsR )
  431.         ).
  432.  
  433.  
  434. /*
  435.    Netvals = current assignments of nets: [n1(1), n5(0),.....,nn(x)]è   Inputnets = input nets to specific gate: [n1,n3,..nx]
  436.    Inputvals = [1,0,.d, db, 0]
  437. */
  438.  
  439. replcbyval( A, B, C, NetVarlist) :- 
  440.                            replcbyval1( A, B, C, [], NetVarlist ), !.
  441.  
  442. replcbyval1( _, [], [], NetVarlist, NetVarlist ).
  443. replcbyval1( Netvals, [Inputnet|Restnets], 
  444.               [Inputval|Restvals], NetVarlist, NetVarR ) :-
  445.     (
  446.           (
  447.             member( Inputnet( Inputval ), Netvals ), 
  448.             NetVarT = NetVarlist
  449.           );
  450.           (
  451.             var( Inputval ),
  452.             NetVarT = [Inputnet(Inputval)|NetVarlist]
  453.           )
  454.         ),
  455.     replcbyval1( Netvals, Restnets, Restvals, NetVarT, NetVarR ).
  456.  
  457. getinps( A, B ) :- 
  458.     inputs( Inplist ),
  459.     getinps1( A, Inplist, [], B ), !, Inplist \= [].
  460.  
  461. getinps1( _, [], Netandvals, Netandvals ).
  462. getinps1( Netvals, [Inputnet|Restnets], Inplistform, Retlist ) :-
  463.     (
  464.           member( Inputnet( Inputval ), Netvals ), 
  465.       getinps1( Netvals, Restnets, 
  466.                    [Inputnet(Inputval)|Inplistform], Retlist )
  467.         );
  468.     getinps1( Netvals, Restnets, Inplistform, Retlist ).
  469.  
  470. getoutp( A, B ) :- 
  471.     outputs( Outplist ),
  472.     getoutp1( A, Outplist, [], B ), !, Outplist \= [].
  473.  
  474. getoutp1( _, [], Netandvals, Netandvals ).
  475. getoutp1( Netvals, [Outputnet|Restnets], Outlistform, Retlist ) :-
  476.     (
  477.           member( Outputnet( Outputval ), Netvals ), 
  478.           (Outputval == d ; Outputval == db),
  479.       getoutp1( Netvals, Restnets, 
  480.                    [Outputnet(Outputval)|Outlistform], Retlist )
  481.         );
  482.     getoutp1( Netvals, Restnets, Outlistform, Retlist ).
  483.  
  484.  
  485.  
  486.  
  487.  
  488. /* funclist = [nx,...,nx],    arglist = [1,0,...,etc] */
  489. pairoff( [], [], Result, Result ).èpairoff( [Func|F_rem], [Arg|Arg_rem], Tlist, Reslist ) :-
  490.     pairoff( F_rem, Arg_rem, [Func(Arg)|Tlist], Reslist ).
  491.  
  492.  
  493. /* Samples:
  494. Type:      and3( pdcfand3, pcand3 ).
  495. Pdcfclass: pdcfand3( sa1(3), db, [[1,1,0]] ).
  496. Gate:      r6( or3, 3, [n25,n26,n28], n34 ).
  497. */
  498.  
  499. appenddef( L1, L2, L3 ) :- append( L1, L2, L3 ), !.
  500. append([],L,L).
  501. append([Z|L1],L2,[Z|L3]) :- append( L1,L2,L3 ).
  502.  
  503.  
  504. /* Non-instantiating member, for lists containing variables: */
  505. vmember( X, List ) :- member( Y, List ), X == Y, !.
  506.  
  507.  
  508.  
  509. revlist( List, Reverse ) :- rev( List, [], Reverse ), !.
  510. rev( [], L, L ).
  511. rev( [H|List], Formlist, Retlist ) :-
  512.     rev( List, [H|Formlist], Retlist ).
  513.  
  514.  
  515.